The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__dbl(0) → 0
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0, cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0) → 0
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
a__sel(0, cons(sel(0, cons(X12842_3, X22843_3)), Y)) →⁺ a__sel(0, cons(X12842_3, X22843_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [X12842_3 / sel(0, cons(X12842_3, X22843_3))].
The result substitution is [Y / X22843_3].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
a__sel, mark

They will be analysed ascendingly in the following order:
a__sel = mark

(8) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(x))

The following defined symbols remain to be analysed:
mark, a__sel

They will be analysed ascendingly in the following order:
a__sel = mark

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol mark.

(10) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(x))

The following defined symbols remain to be analysed:
a__sel

They will be analysed ascendingly in the following order:
a__sel = mark

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol a__sel.

(12) Obligation:

TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)

Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from

Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(x))

No more defined symbols left to analyse.